Nuprl Definition : idlnk-deq
0,22
postcript
pdf
IdLnkDeq == product-deq(Id;Id
Id;IdDeq;product-deq(Id;Id;IdDeq;IdDeq))
latex
Definitions
x
:
A
B
(
x
)
,
product-deq(
A
;
B
;
a
;
b
)
,
Id
,
IdDeq
FDL editor aliases
idlnk-deq
origin
Id;IdDeq;product-deq(Id;Id;IdDeq;IdDeq)) Id;IdDeq;product-deq(Id;Id;IdDeq;IdDeq)) B(x)